$\forall$${\it the\_es}$:event\_system\{i:l\}, $e$,${\it e'}$,$y$:es{-}E(${\it the\_es}$).
\\[0ex]l\_before(${\it e'}$; $y$; before($e$); es{-}E(${\it the\_es}$))
\\[0ex]$\Leftarrow\!\Rightarrow$ (es{-}locl(${\it the\_es}$; ${\it e'}$; $y$) $\wedge$ es{-}locl(${\it the\_es}$; $y$; $e$))